Automated Theorem Proving (ATP) is an established branch of ArtificialIntelligence. The purpose of ATP is to design a system which can automaticallyfigure out an algorithm either to prove or disprove a mathematical claim, onthe basis of a set of given premises, using a set of fundamental postulates andfollowing the method of logical inference. In this paper, we propose GraATP, ageneralized framework for automated theorem proving in plane geometry. Ourproposed method translates the geometric entities into nodes of a graph and therelations between them as edges of that graph. The automated system searchesfor different ways to reach the conclusion for a claim via graph traversal bywhich the validity of the geometric theorem is examined.
展开▼
